Nuprl Lemma : ecl-trans-state-append 0,22
ds:x:Id fp Type, da:k:Knd fp Type, v:ecl-trans-tuple{i:l}(ds;da), L1, L2:Top List.
ecl-trans-state(v;L1 @ L2) ~ ecl-trans-state-from(v;ecl-trans-state(v;L1);L2) 
latex

Definitionst  T, Top, x:A. B(x), ecl-trans-state(v;L), Id, x. t(x), a:A fp B(a), Knd, ecl-trans-tuple{i:l}(ds;da)
Lemmastop wf, ecl-trans-tuple wf, Knd wf, fpf wf, Id wf, ecl-trans-state-from-append

origin